Nuprl Lemma : sends-msgs_wf
0,22
postcript
pdf
A
,
T
:Type,
B
:(Id
Type),
s
:
A
,
v
:
T
,
tgf
:(
tg
:Id
(
A
T
(
B
(
tg
) List))).
sends-msgs(
s
;
v
;
tgf
)
(
tg
:Id
B
(
tg
)) List
latex
Definitions
t
T
,
Id
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
2of(
t
)
,
1of(
t
)
,
map(
f
;
as
)
,
sends-msgs(
s
;
v
;
tg_f
)
Lemmas
map
wf
,
pi1
wf
,
pi2
wf
,
Id
wf
origin
A, T:Type, B:(Id
Type), s:A, v:T, tgf:(tg:Id
(AT(B(tg) List))).
(tg:IdB(tg)) List A, T:Type, B:(IdType), s:A, v:T, tgf:(tg:Id(AT(B(tg) List))).
(tg:IdB(tg)) List Tx:A. B(x)
x. t(x)